Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(0)  → 0
2:    f(s(0))  → s(0)
3:    f(s(s(x)))  → p(h(g(x)))
4:    g(0)  → pair(s(0),s(0))
5:    g(s(x))  → h(g(x))
6:    h(x)  → pair(p(x) + q(x),p(x))
7:    p(pair(x,y))  → x
8:    q(pair(x,y))  → y
9:    x + 0  → x
10:    x + s(y)  → s(x + y)
11:    f(s(s(x)))  → p(g(x)) + q(g(x))
12:    g(s(x))  → pair(p(g(x)) + q(g(x)),p(g(x)))
There are 15 dependency pairs:
13:    F(s(s(x)))  → P(h(g(x)))
14:    F(s(s(x)))  → H(g(x))
15:    G(s(x))  → H(g(x))
16:    H(x)  → p(x) +# q(x)
17:    H(x)  → Q(x)
18:    H(x)  → P(x)
19:    x +# s(y)  → x +# y
20:    F(s(s(x)))  → p(g(x)) +# q(g(x))
21:    F(s(s(x)))  → P(g(x))
22:    F(s(s(x)))  → Q(g(x))
23:    F(s(s(x)))  → G(x)
24:    G(s(x))  → p(g(x)) +# q(g(x))
25:    G(s(x))  → Q(g(x))
26:    G(s(x))  → P(g(x))
27:    G(s(x))  → G(x)
The approximated dependency graph contains 2 SCCs: {19} and {27}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006